1. Technical Field
The present disclosure relates to a system and method for automatically verifying determinism of structured parallel programs.
2. Discussion of Related Art
One difficulty in parallel programming is the need to reason about possible interleavings of concurrent operations. Typically, the number of interleavings, even for small programs, makes this task difficult. To simplify reasoning about parallel programs, it is desirable to reduce the number of interleavings that need to be consider. One way to achieve that is to require parallel programs to be deterministic. Informally, determinism means that for a given input state, the parallel program will always produce the same output state. Determinism is an attractive correctness property as it abstracts away the interleavings underlying a computation.